The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil

The (relative) TRS S consists of the following rules:

#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil

The (relative) TRS S consists of the following rules:

#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
#compare, findMin, findMin#1, minSort, minSort#1

They will be analysed ascendingly in the following order:
findMin = findMin#1
findMin < minSort
minSort = minSort#1

(6) Obligation:

Innermost TRS:
Rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil

Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))

The following defined symbols remain to be analysed:
#compare, findMin, findMin#1, minSort, minSort#1

They will be analysed ascendingly in the following order:
findMin = findMin#1
findMin < minSort
minSort = minSort#1

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)

Induction Base:
#compare(gen_#0:#neg:#pos:#s5_4(0), gen_#0:#neg:#pos:#s5_4(0)) →_R^Ω(0)
#EQ

Induction Step:
#compare(gen_#0:#neg:#pos:#s5_4(+(n8_4, 1)), gen_#0:#neg:#pos:#s5_4(+(n8_4, 1))) →_R^Ω(0)
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) →_IH
#EQ

We have rt ∈ Ω(1) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n⁰).

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
Rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))

The following defined symbols remain to be analysed:
findMin#1, findMin, minSort, minSort#1

They will be analysed ascendingly in the following order:
findMin = findMin#1
findMin < minSort
minSort = minSort#1

(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
findMin#1(gen_:::nil6_4(n318853_4)) → *7_4, rt ∈ Ω(n318853₄)

Induction Base:
findMin#1(gen_:::nil6_4(0))

Induction Step:
findMin#1(gen_:::nil6_4(+(n318853_4, 1))) →_R^Ω(1)
findMin#2(findMin(gen_:::nil6_4(n318853_4)), #0) →_R^Ω(1)
findMin#2(findMin#1(gen_:::nil6_4(n318853_4)), #0) →_IH
findMin#2(*7_4, #0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(11) Complex Obligation (BEST)

(12) Obligation:

Innermost TRS:
Rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n318853_4)) → *7_4, rt ∈ Ω(n318853₄)

Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))

The following defined symbols remain to be analysed:
findMin, minSort, minSort#1

They will be analysed ascendingly in the following order:
findMin = findMin#1
findMin < minSort
minSort = minSort#1

(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
findMin(gen_:::nil6_4(n321980_4)) → *7_4, rt ∈ Ω(n321980₄)

Induction Base:
findMin(gen_:::nil6_4(0))

Induction Step:
findMin(gen_:::nil6_4(+(n321980_4, 1))) →_R^Ω(1)
findMin#1(gen_:::nil6_4(+(n321980_4, 1))) →_R^Ω(1)
findMin#2(findMin(gen_:::nil6_4(n321980_4)), #0) →_IH
findMin#2(*7_4, #0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(14) Complex Obligation (BEST)

(15) Obligation:

Innermost TRS:
Rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n318853_4)) → *7_4, rt ∈ Ω(n318853₄)
findMin(gen_:::nil6_4(n321980_4)) → *7_4, rt ∈ Ω(n321980₄)

Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))

The following defined symbols remain to be analysed:
findMin#1, minSort, minSort#1

They will be analysed ascendingly in the following order:
findMin = findMin#1
findMin < minSort
minSort = minSort#1

(16) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
findMin#1(gen_:::nil6_4(n326993_4)) → *7_4, rt ∈ Ω(n326993₄)

Induction Base:
findMin#1(gen_:::nil6_4(0))

Induction Step:
findMin#1(gen_:::nil6_4(+(n326993_4, 1))) →_R^Ω(1)
findMin#2(findMin(gen_:::nil6_4(n326993_4)), #0) →_R^Ω(1)
findMin#2(findMin#1(gen_:::nil6_4(n326993_4)), #0) →_IH
findMin#2(*7_4, #0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(17) Complex Obligation (BEST)

(18) Obligation:

Innermost TRS:
Rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n326993_4)) → *7_4, rt ∈ Ω(n326993₄)
findMin(gen_:::nil6_4(n321980_4)) → *7_4, rt ∈ Ω(n321980₄)

Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))

The following defined symbols remain to be analysed:
minSort#1, minSort

They will be analysed ascendingly in the following order:
minSort = minSort#1

(19) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol minSort#1.

(20) Obligation:

Innermost TRS:
Rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n326993_4)) → *7_4, rt ∈ Ω(n326993₄)
findMin(gen_:::nil6_4(n321980_4)) → *7_4, rt ∈ Ω(n321980₄)

Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))

The following defined symbols remain to be analysed:
minSort

They will be analysed ascendingly in the following order:
minSort = minSort#1

(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol minSort.

(22) Obligation:

Innermost TRS:
Rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n326993_4)) → *7_4, rt ∈ Ω(n326993₄)
findMin(gen_:::nil6_4(n321980_4)) → *7_4, rt ∈ Ω(n321980₄)

Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))

No more defined symbols left to analyse.

(23) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
findMin#1(gen_:::nil6_4(n326993_4)) → *7_4, rt ∈ Ω(n326993₄)

(24) BOUNDS(n^1, INF)

(25) Obligation:

Innermost TRS:
Rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n326993_4)) → *7_4, rt ∈ Ω(n326993₄)
findMin(gen_:::nil6_4(n321980_4)) → *7_4, rt ∈ Ω(n321980₄)

Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))

No more defined symbols left to analyse.

(26) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
findMin#1(gen_:::nil6_4(n326993_4)) → *7_4, rt ∈ Ω(n326993₄)

(27) BOUNDS(n^1, INF)

(28) Obligation:

Innermost TRS:
Rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n318853_4)) → *7_4, rt ∈ Ω(n318853₄)
findMin(gen_:::nil6_4(n321980_4)) → *7_4, rt ∈ Ω(n321980₄)

Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))

No more defined symbols left to analyse.

(29) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
findMin#1(gen_:::nil6_4(n318853_4)) → *7_4, rt ∈ Ω(n318853₄)

(30) BOUNDS(n^1, INF)

(31) Obligation:

Innermost TRS:
Rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)
findMin#1(gen_:::nil6_4(n318853_4)) → *7_4, rt ∈ Ω(n318853₄)

Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))

No more defined symbols left to analyse.

(32) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
findMin#1(gen_:::nil6_4(n318853_4)) → *7_4, rt ∈ Ω(n318853₄)

(33) BOUNDS(n^1, INF)

(34) Obligation:

Innermost TRS:
Rules:
#less(@x, @y) → #cklt(#compare(@x, @y))
findMin(@l) → findMin#1(@l)
findMin#1(::(@x, @xs)) → findMin#2(findMin(@xs), @x)
findMin#1(nil) → nil
findMin#2(::(@y, @ys), @x) → findMin#3(#less(@x, @y), @x, @y, @ys)
findMin#2(nil, @x) → ::(@x, nil)
findMin#3(#false, @x, @y, @ys) → ::(@y, ::(@x, @ys))
findMin#3(#true, @x, @y, @ys) → ::(@x, ::(@y, @ys))
minSort(@l) → minSort#1(findMin(@l))
minSort#1(::(@x, @xs)) → ::(@x, minSort(@xs))
minSort#1(nil) → nil
#cklt(#EQ) → #false
#cklt(#GT) → #false
#cklt(#LT) → #true
#compare(#0, #0) → #EQ
#compare(#0, #neg(@y)) → #GT
#compare(#0, #pos(@y)) → #LT
#compare(#0, #s(@y)) → #LT
#compare(#neg(@x), #0) → #LT
#compare(#neg(@x), #neg(@y)) → #compare(@y, @x)
#compare(#neg(@x), #pos(@y)) → #LT
#compare(#pos(@x), #0) → #GT
#compare(#pos(@x), #neg(@y)) → #GT
#compare(#pos(@x), #pos(@y)) → #compare(@x, @y)
#compare(#s(@x), #0) → #GT
#compare(#s(@x), #s(@y)) → #compare(@x, @y)

Types:
#less :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #false:#true
#cklt :: #EQ:#GT:#LT → #false:#true
#compare :: #0:#neg:#pos:#s → #0:#neg:#pos:#s → #EQ:#GT:#LT
findMin :: :::nil → :::nil
findMin#1 :: :::nil → :::nil
:: :: #0:#neg:#pos:#s → :::nil → :::nil
findMin#2 :: :::nil → #0:#neg:#pos:#s → :::nil
nil :: :::nil
findMin#3 :: #false:#true → #0:#neg:#pos:#s → #0:#neg:#pos:#s → :::nil → :::nil
#false :: #false:#true
#true :: #false:#true
minSort :: :::nil → :::nil
minSort#1 :: :::nil → :::nil
#EQ :: #EQ:#GT:#LT
#GT :: #EQ:#GT:#LT
#LT :: #EQ:#GT:#LT
#0 :: #0:#neg:#pos:#s
#neg :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#pos :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
#s :: #0:#neg:#pos:#s → #0:#neg:#pos:#s
hole_#false:#true1_4 :: #false:#true
hole_#0:#neg:#pos:#s2_4 :: #0:#neg:#pos:#s
hole_#EQ:#GT:#LT3_4 :: #EQ:#GT:#LT
hole_:::nil4_4 :: :::nil
gen_#0:#neg:#pos:#s5_4 :: Nat → #0:#neg:#pos:#s
gen_:::nil6_4 :: Nat → :::nil

Lemmas:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)

Generator Equations:
gen_#0:#neg:#pos:#s5_4(0) ⇔ #0
gen_#0:#neg:#pos:#s5_4(+(x, 1)) ⇔ #neg(gen_#0:#neg:#pos:#s5_4(x))
gen_:::nil6_4(0) ⇔ nil
gen_:::nil6_4(+(x, 1)) ⇔ ::(#0, gen_:::nil6_4(x))

No more defined symbols left to analyse.

(35) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(1) was proven with the following lemma:
#compare(gen_#0:#neg:#pos:#s5_4(n8_4), gen_#0:#neg:#pos:#s5_4(n8_4)) → #EQ, rt ∈ Ω(0)

(36) BOUNDS(1, INF)